decl{-}state(${\it ds}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$x$:Id$\rightarrow$fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)